T:Type, R:(TT), x, y, z:T. (x R y)  (y (R^*) z)  (x R^+ z) 

latex

Definitions	R^*, R^+, P  Q, , , rel_exp(T;R;n), x:A. B(x), x f y, f(a), x:AB(x), , t  T, Type, x:A. B(x), x:A  B(x), n+m, #$n, a < b, {x:A| B(x)} , , A  B, A, False, P  Q, P  Q, P  Q, Void, A c B, P & Q, s = t, T, n - m, True
Lemmas	le wf, rel exp iff2, nat plus inc, rel exp wf, nat wf